$\forall$${\it es}$:ES, $P$, $Q$:(E$\rightarrow\mathbb{P}$), $f$:(\{$e$:E$\mid$ $P$($e$)\} $\rightarrow$\{$e$:E$\mid$ $Q$($e$)\} ), $T$, ${\it T'}$:Type, $R$:($T$$\rightarrow$${\it T'}$$\rightarrow\mathbb{P}$).
\\[0ex]($\forall$$e$:E. $P$($e$) $\Rightarrow$ (valtype($e$) $\subseteq$r $T$))
\\[0ex]$\Rightarrow$ ($\forall$$e$:E. $Q$($e$) $\Rightarrow$ (valtype($e$) $\subseteq$r ${\it T'}$))
\\[0ex]$\Rightarrow$ (($e$.$P$($e$) $\rightarrow$$e$.$f$($e$)$\rightarrow$ $e$.$Q$($e$)) with $R$ $\in$ $\mathbb{P}$)